1  /-
  2  Copyright (c) 2019 Kenny Lau. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Kenny Lau
  5  
  6  Integral closure of a subring.
  7  -/
  8  
  9  import ring_theory.adjoin linear_algebra.finsupp
src         └────────────────┘ └────────────────────┘
 10  
 11  universes u v
 12  
 13  open_locale classical
 14  open polynomial submodule
 15  
 16  section
 17  variables (R : Type u) {A : Type v}
 18  variables [comm_ring R] [comm_ring A]
 19  variables [algebra R A]
id              └─────┘
src             └─────┘
typ             └─────┘
doc             └─────┘
 20  
 21  def is_integral (x : A) : Prop :=
id                        
typ                       
 22  ∃ p : polynomial R, monic p ∧ aeval R A x p = 0
id        └────────┘  └───┘   └───┘     
src       └────────┘   └───┘    └───┘         
typ       └────────┘  └───┘   └───┘     
doc        └────────┘    └───┘     └───┘
 23  
 24  variables {R}
 25  theorem is_integral_algebra_map {x : R} : is_integral R (algebra_map A x) :=
id                                            └─────────┘   └─────────┘  
src                                            └─────────┘    └─────────┘
typ                                           └─────────┘   └─────────┘  
 26  ⟨X - C x, monic_X_sub_C _,
id         └───────────┘
src         └───────────┘
typ        └───────────┘
doc      
 27  by rw [alg_hom.map_sub, aeval_def, aeval_def, eval₂_X, eval₂_C, sub_self]⟩
id          └─────────────┘  └───────┘  └───────┘  └─────┘  └─────┘  └──────┘
src     └──┘└─────────────┘└┘└───────┘└┘└───────┘└┘└─────┘└┘└─────┘└┘└──────┘
typ     └──┘└─────────────┘└┘└───────┘└┘└───────┘└┘└─────┘└┘└─────┘└┘└──────┘
doc     └──┘               └┘         └┘         └┘       └┘       └┘        
txt     └──┘               └┘         └┘         └┘       └┘       └┘        
par     └──┘               └┘         └┘         └┘       └┘       └┘        
pid       └┘               └┘         └┘         └┘       └┘       └┘        
st     └──────────────────┘└─────────┘└─────────┘└───────┘└───────┘└────────┘
 28  
 29  theorem is_integral_of_subring {x : A} (T : set R) [is_subring T]
id                                              └─┘    └────────┘ 
src                                              └─┘     └────────┘
typ                                             └─┘    └────────┘ 
doc                                                      └────────┘
 30    (hx : is_integral T (algebra.comap.to_comap T R A x)) : is_integral R (x : A) :=
id           └─────────┘   └────────────────────┘         └─────────┘      
src          └─────────┘    └────────────────────┘             └─────────┘
typ          └─────────┘   └────────────────────┘         └─────────┘      
 31  let ⟨p, hpm, hpx⟩ := hx in
id   └─┘    └─┘  └─┘     └┘
typ  └─┘    └─┘  └─┘     └┘
 32  ⟨⟨p.support, λ n, (p.to_fun n).1,
id      └──────┘        └─────┘  
src     └──────┘         └─────┘   
typ     └──────┘        └─────┘  
 33    λ n, finsupp.mem_support_iff.trans (not_iff_not_of_iff
id         └─────────────────────┘└────┘  └────────────────┘
src         └─────────────────────┘└────┘  └────────────────┘
typ        └─────────────────────┘└────┘  └────────────────┘
 34      ⟨λ H, have _ := congr_arg subtype.val H, this,
id                      └───────┘ └─────────┘   └──┘
src                      └───────┘ └─────────┘
typ                     └───────┘ └─────────┘   └──┘
 35      λ H, subtype.eq H⟩)⟩,
id           └────────┘ 
src           └────────┘
typ          └────────┘ 
 36  have _ := congr_arg subtype.val hpm, this, hpx⟩
id             └───────┘ └─────────┘      └──┘
src            └───────┘ └─────────┘
typ            └───────┘ └─────────┘      └──┘
 37  
 38  theorem is_integral_iff_is_integral_closure_finite {r : A} :
id                                                           
typ                                                          
 39    is_integral R r ↔ ∃ s : set R, s.finite ∧
id     └─────────┘         └─┘  └─────┘ 
src    └─────────┘           └─┘    └─────┘ 
typ    └─────────┘         └─┘  └─────┘ 
doc                                    └─────┘
 40      is_integral (ring.closure s) (algebra.comap.to_comap (ring.closure s) R A r) :=
id       └─────────┘  └──────────┘    └────────────────────┘  └──────────┘     
src      └─────────┘  └──────────┘     └────────────────────┘  └──────────┘
typ      └─────────┘  └──────────┘    └────────────────────┘  └──────────┘     
 41  begin
st   └─────
 42    split; intro hr,
src    └───┘  └──────┘
typ    └───┘  └──────┘
doc    └───┘  └──────┘
txt    └───┘  └──────┘
par    └───┘  └──────┘
pid                └─┘
st   ────────────────┘└─
 43    { rcases hr with ⟨p, hmp, hpr⟩,
id              └┘
src      └─────┘  └─────────────────┘
typ      └─────┘└┘└─────────────────┘
doc      └─────┘  └─────────────────┘
txt      └─────┘  └─────────────────┘
par      └─────┘  └─────────────────┘
pid              └─────────────────┘
st   ───┘└──────────────────────────┘└─
 44      exact ⟨_, set.finite_mem_finset _, p.restriction, subtype.eq hmp, hpr⟩ },
id                 └───────────────────┘    └───────────┘  └────────┘ └─┘  └─┘
src      └────┘ └─┘└───────────────────┘└──┘└───────────┘└┘└────────┘   └┘   └┘
typ      └────┘ └─┘└───────────────────┘└──┘└───────────┘└┘└────────┘└─┘└┘└─┘└┘
doc      └────┘ └─┘                     └──┘└───────────┘└┘             └┘   └┘
txt      └────┘ └─┘                     └──┘             └┘             └┘   └┘
par      └────┘ └─┘                     └──┘             └┘             └┘   └┘
pid            └─┘                     └──┘             └┘             └┘   
st   ──────────────────────────────────────────────────────────────────────────┘└┘
 45    rcases hr with ⟨s, hs, hsr⟩,
id            └┘
src    └─────┘  └────────────────┘
typ    └─────┘└┘└────────────────┘
doc    └─────┘  └────────────────┘
txt    └─────┘  └────────────────┘
par    └─────┘  └────────────────┘
pid            └────────────────┘
st   ────────────────────────────┘└─
 46    exact is_integral_of_subring _ hsr
id           └────────────────────┘   └─┘
src    └────┘└────────────────────┘└─┘   
typ    └────┘└────────────────────┘└─┘└─┘
doc    └────┘                      └─┘   
txt    └────┘                      └─┘   
par    └────┘                      └─┘   
pid                               └─┘   
st   ────────────────────────────────────┘
 47  end
st   └─┘
 48  
 49  theorem fg_adjoin_singleton_of_integral (x : A) (hx : is_integral R x) :
id                                                        └─────────┘  
src                                                        └─────────┘
typ                                                       └─────────┘  
 50    (algebra.adjoin R ({x} : set A) : submodule R A).fg :=
id      └────────────┘       └─┘     └───────┘   └┘
src     └────────────┘         └─┘      └───────┘     └┘
typ     └────────────┘       └─┘     └───────┘   └┘
doc                                      └───────┘
 51  begin
st   └─────
 52    rcases hx with ⟨f, hfm, hfx⟩,
id            └┘
src    └─────┘  └─────────────────┘
typ    └─────┘└┘└─────────────────┘
doc    └─────┘  └─────────────────┘
txt    └─────┘  └─────────────────┘
par    └─────┘  └─────────────────┘
pid            └─────────────────┘
st   ─────────────────────────────┘└─
 53    existsi finset.image ((^) x) (finset.range (nat_degree f + 1)),
id             └──────────┘        └──────────┘  └────────┘  
src    └──────┘└──────────┘ └─┘ └┘ └──────────┘ └────────┘ └──┘
typ    └──────┘└──────────┘ └─┘└┘ └──────────┘ └────────┘└──┘
doc    └──────┘└──────────┘  └─┘ └┘ └──────────┘ └────────┘  └──┘
txt    └──────┘              └─┘ └┘                          └──┘
par    └──────┘              └─┘ └┘                          └──┘
pid                         └─┘ └┘                          └──┘
st   ───────────────────────────────────────────────────────────────┘└─
 54    apply le_antisymm,
id           └─────────┘
src    └────┘└─────────┘
typ    └────┘└─────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ──────────────────┘└─
 55    { rw span_le, intros s hs, rw finset.mem_coe at hs,
id          └─────┘                  └────────────┘
src      └─┘└─────┘  └─────────┘  └─┘└────────────┘└────┘
typ      └─┘└─────┘  └─────────┘  └─┘└────────────┘└────┘
doc      └─┘         └─────────┘  └─┘              └────┘
txt      └─┘         └─────────┘  └─┘              └────┘
par      └─┘         └─────────┘  └─┘              └────┘
pid                       └───┘                  └────┘
st   ───┘└────────┘└───────────┘└───────────────────────┘└─
 56      rcases finset.mem_image.1 hs with ⟨k, hk, rfl⟩, clear hk,
id              └──────────────┘   └┘
src      └─────┘└──────────────┘└─┘  └────────────────┘  └──────┘
typ      └─────┘└──────────────┘└─┘└┘└────────────────┘  └──────┘
doc      └─────┘                └─┘  └────────────────┘  └──────┘
txt      └─────┘                └─┘  └────────────────┘  └──────┘
par      └─────┘                └─┘  └────────────────┘  └──────┘
pid                            └─┘  └────────────────┘       └─┘
st   ─────────────────────────────────────────────────┘└────────┘└─
 57      exact is_submonoid.pow_mem (algebra.subset_adjoin (set.mem_singleton _)) },
id             └──────────────────┘  └───────────────────┘  └───────────────┘
src      └────┘└──────────────────┘ └───────────────────┘ └───────────────┘└───┘
typ      └────┘└──────────────────┘ └───────────────────┘ └───────────────┘└───┘
doc      └────┘└──────────────────┘                                        └───┘
txt      └────┘                                                            └───┘
par      └────┘                                                            └───┘
pid                                                                       └──┘
st   ────────────────────────────────────────────────────────────────────────────┘└┘
 58    intros r hr, change r ∈ algebra.adjoin R ({x} : set A) at hr,
id                           └────────────┘        └─┘ 
src    └─────────┘  └─────┘ └────────────┘  └───┘└─┘ └─────┘
typ    └─────────┘  └─────┘└────────────┘ └───┘└─┘└─────┘
doc    └─────────┘  └─────┘                   └───┘    └─────┘
txt    └─────────┘  └─────┘                   └───┘    └─────┘
par    └─────────┘  └─────┘                   └───┘    └─────┘
pid          └───┘                           └───┘    └───┘
st   ────────────┘└───────────────────────────────────────────────┘└─
 59    rw algebra.adjoin_singleton_eq_range at hr, rcases hr with ⟨p, rfl⟩,
id        └───────────────────────────────┘               └┘
src    └─┘└───────────────────────────────┘└────┘  └─────┘  └────────────┘
typ    └─┘└───────────────────────────────┘└────┘  └─────┘└┘└────────────┘
doc    └─┘                                 └────┘  └─────┘  └────────────┘
txt    └─┘                                 └────┘  └─────┘  └────────────┘
par    └─┘                                 └────┘  └─────┘  └────────────┘
pid                                       └────┘          └────────────┘
st   ───────────────────────────────────────────┘└───────────────────────┘└─
 60    rw ← mod_by_monic_add_div p hfm,
id          └──────────────────┘  └─┘
src    └───┘└──────────────────┘ 
typ    └───┘└──────────────────┘└─┘
doc    └───┘                     
txt    └───┘                     
par    └───┘                     
pid      └─┘                     
st   ────────────────────────────────┘└─
 61    rw [alg_hom.map_add, alg_hom.map_mul, hfx, zero_mul, add_zero],
id         └─────────────┘  └─────────────┘  └─┘  └──────┘  └──────┘
src    └──┘└─────────────┘└┘└─────────────┘└┘   └┘└──────┘└┘└──────┘
typ    └──┘└─────────────┘└┘└─────────────┘└┘└─┘└┘└──────┘└┘└──────┘
doc    └──┘               └┘               └┘   └┘        └┘        
txt    └──┘               └┘               └┘   └┘        └┘        
par    └──┘               └┘               └┘   └┘        └┘        
pid      └┘               └┘               └┘   └┘        └┘        
st   ────────────────────┘└───────────────┘└───┘└────────┘└────────┘└──
 62    have : degree (p %ₘ f) ≤ degree f := degree_mod_by_monic_le p hfm,
id                     └┘     └────┘     └────────────────────┘  └─┘
src    └─────┘        └┘ └┘└────┘ └──┘└────────────────────┘ 
typ    └─────┘       └┘ └┘└────┘└──┘└────────────────────┘└─┘
doc    └─────┘        └┘ └┘ └────┘ └──┘                       
txt    └─────┘           └┘        └──┘                       
par    └─────┘           └┘        └──┘                       
pid    └───┘└┘           └┘        └──┘                       
st   ──────────────────────────────────────────────────────────────────┘└─
 63    generalize_hyp : p %ₘ f = q at this ⊢,
id                          
src    └───────────────┘      └────────┘
typ    └───────────────┘    └────────┘
doc    └───────────────┘      └────────┘
txt    └───────────────┘      └────────┘
par    └───────────────┘      └────────┘
pid                        └────────┘
st   ──────────────────────────────────────┘└─
 64    rw [← sum_C_mul_X_eq q, aeval_def, eval₂_sum, finsupp.sum, mem_coe],
id           └────────────┘   └───────┘  └───────┘  └─────────┘  └─────┘
src    └────┘└────────────┘ └┘└───────┘└┘└───────┘└┘└─────────┘└┘└─────┘
typ    └────┘└────────────┘└┘└───────┘└┘└───────┘└┘└─────────┘└┘└─────┘
doc    └────┘               └┘         └┘         └┘└─────────┘└┘       
txt    └────┘               └┘         └┘         └┘           └┘       
par    └────┘               └┘         └┘         └┘           └┘       
pid      └──┘               └┘         └┘         └┘           └┘       
st   ───────────────────────┘└─────────┘└─────────┘└───────────┘└───────┘└──
 65    refine sum_mem _ (λ k hkq, _),
id            └─────┘
src    └─────┘└─────┘└─┘  └────────┘
typ    └─────┘└─────┘└─┘  └────────┘
doc    └─────┘       └─┘  └────────┘
txt    └─────┘       └─┘  └────────┘
par    └─────┘       └─┘  └────────┘
pid                 └─┘  └────────┘
st   ──────────────────────────────┘└─
 66    rw [eval₂_mul, eval₂_C, eval₂_pow, eval₂_X, ← algebra.smul_def],
id         └───────┘  └─────┘  └───────┘  └─────┘    └──────────────┘
src    └──┘└───────┘└┘└─────┘└┘└───────┘└┘└─────┘└──┘└──────────────┘
typ    └──┘└───────┘└┘└─────┘└┘└───────┘└┘└─────┘└──┘└──────────────┘
doc    └──┘         └┘       └┘         └┘       └──┘                
txt    └──┘         └┘       └┘         └┘       └──┘                
par    └──┘         └┘       └┘         └┘       └──┘                
pid      └┘         └┘       └┘         └┘       └──┘                
st   ──────────────┘└───────┘└─────────┘└───────┘└──────────────────┘└──
 67    refine smul_mem _ _ (subset_span _),
id            └──────┘      └─────────┘
src    └─────┘└──────┘└───┘ └─────────┘└─┘
typ    └─────┘└──────┘└───┘ └─────────┘└─┘
doc    └─────┘        └───┘            └─┘
txt    └─────┘        └───┘            └─┘
par    └─────┘        └───┘            └─┘
pid                  └───┘            └─┘
st   ────────────────────────────────────┘└─
 68    rw finset.mem_coe, refine finset.mem_image.2 ⟨_, _, rfl⟩,
id        └────────────┘         └──────────────┘          └─┘
src    └─┘└────────────┘  └─────┘└──────────────┘└─┘ └────┘└─┘
typ    └─┘└────────────┘  └─────┘└──────────────┘└─┘ └────┘└─┘
doc    └─┘                └─────┘                └─┘ └────┘   
txt    └─┘                └─────┘                └─┘ └────┘   
par    └─┘                └─────┘                └─┘ └────┘   
pid                                            └─┘ └────┘   
st   ──────────────────┘└─────────────────────────────────────┘└─
 69    rw [finset.mem_range, nat.lt_succ_iff], refine le_of_not_lt (λ hk, _),
id         └──────────────┘  └─────────────┘          └──────────┘
src    └──┘└──────────────┘└┘└─────────────┘  └─────┘└──────────┘  └─────┘
typ    └──┘└──────────────┘└┘└─────────────┘  └─────┘└──────────┘  └─────┘
doc    └──┘                └┘                 └─────┘              └─────┘
txt    └──┘                └┘                 └─────┘              └─────┘
par    └──┘                └┘                 └─────┘              └─────┘
pid      └┘                └┘                                     └─────┘
st   ─────────────────────┘└───────────────┘└──────────────────────────────┘└─
 70    rw [degree_le_iff_coeff_zero] at this,
id         └──────────────────────┘
src    └──┘└──────────────────────┘└───────┘
typ    └──┘└──────────────────────┘└───────┘
doc    └──┘                        └───────┘
txt    └──┘                        └───────┘
par    └──┘                        └───────┘
pid      └┘                        └──────┘
st   ─────────────────────────────┘└──────┘└─
 71    rw [finsupp.mem_support_iff] at hkq, apply hkq, apply this,
id         └─────────────────────┘
src    └──┘└─────────────────────┘└──────┘  └────┘     └────┘
typ    └──┘└─────────────────────┘└──────┘  └────┘     └────┘
doc    └──┘                       └──────┘  └────┘     └────┘
txt    └──┘                       └──────┘  └────┘     └────┘
par    └──┘                       └──────┘  └────┘     └────┘
pid      └┘                       └─────┘                 
st   ────────────────────────────┘└─────┘└─────────┘└──────────┘└─
 72    exact lt_of_le_of_lt degree_le_nat_degree (with_bot.coe_lt_coe.2 hk)
id           └────────────┘ └──────────────────┘  └─────────────────┘   └┘
src    └────┘└────────────┘└──────────────────┘ └─────────────────┘└─┘  └┘
typ    └────┘└────────────┘└──────────────────┘ └─────────────────┘└─┘└┘└┘
doc    └────┘                                                      └─┘  └┘
txt    └────┘                                                      └─┘  └┘
par    └────┘                                                      └─┘  └┘
pid                                                               └─┘  
st   ──────────────────────────────────────────────────────────────────────┘
 73  end
st   └─┘
 74  
 75  theorem fg_adjoin_of_finite {s : set A} (hfs : s.finite)
id                                    └─┘          └─────┘
src                                   └─┘            └─────┘
typ                                   └─┘          └─────┘
doc                                                  └─────┘
 76    (his : ∀ x ∈ s, is_integral R x) : (algebra.adjoin R s : submodule R A).fg :=
id                   └─────────┘       └────────────┘     └───────┘   └┘
src                   └─────────┘         └────────────┘       └───────┘     └┘
typ                  └─────────┘       └────────────┘     └───────┘   └┘
doc                                                             └───────┘
 77  set.finite.induction_on hfs (λ _, ⟨finset.singleton 1, le_antisymm
id   └─────────────────────┘ └─┘       └──────────────┘    └─────────┘
src  └─────────────────────┘            └──────────────┘    └─────────┘
typ  └─────────────────────┘ └─┘       └──────────────┘    └─────────┘
doc                                     └──────────────┘
 78    (span_le.2 $ set.singleton_subset_iff.2 $ is_submonoid.one_mem _)
id      └─────┘    └──────────────────────┘    └──────────────────┘
src     └─────┘    └──────────────────────┘    └──────────────────┘
typ     └─────┘    └──────────────────────┘    └──────────────────┘
 79    (show ring.closure _ ⊆ _, by rw set.union_empty; exact
id           └──────────┘             └─────────────┘
src          └──────────┘          └─┘└─────────────┘  └─────
typ          └──────────┘          └─┘└─────────────┘  └─────
doc                                 └─┘                 └─────
txt                                 └─┘                 └─────
par                                 └─┘                 └─────
pid                                                         
st                                 └──────────────────────────
 80      set.subset.trans (ring.closure_subset (set.subset.refl _))
id       └──────────────┘  └─────────────────┘  └─────────────┘
src  ───┘└──────────────┘ └─────────────────┘ └─────────────┘└────
typ  ───┘└──────────────┘ └─────────────────┘ └─────────────┘└────
doc  ───┘                                                    └────
txt  ───┘                                                    └────
par  ───┘                                                    └────
pid  ───┘                                                    └────
st   ───────────────────────────────────────────────────────────────
 81      (λ y ⟨x, hx⟩, hx ▸ mul_one (algebra_map A x) ▸ algebra.smul_def x (1:A) ▸ (mem_coe _).2
id               └┘       └─────┘  └─────────┘        └──────────────┘           └─────┘
src  ───┘  └──┘ └┘  └─┘  └─────┘ └─────────┘  └┘ └──────────────┘  └┘ └┘  └─────┘└─────
typ  ───┘  └──┘└┘└┘└─┘  └─────┘ └─────────┘  └┘ └──────────────┘  └┘└┘  └─────┘└─────
doc  ───┘  └──┘ └┘  └─┘                        └┘                   └┘ └┘         └─────
txt  ───┘  └──┘ └┘  └─┘                        └┘                   └┘ └┘         └─────
par  ───┘  └──┘ └┘  └─┘                        └┘                   └┘ └┘         └─────
pid  ───┘  └──┘ └┘  └─┘                        └┘                   └┘ └┘         └─────
st   ────────────────────────────────────────────────────────────────────────────────────────────
 82        (submodule.smul_mem _ x $ subset_span $ or.inl rfl)))⟩)
id          └────────────────┘       └─────────┘   └────┘ └─┘
src  ─────┘ └────────────────┘└─┘  └─────────┘ └────┘└─┘└┘
typ  ─────┘ └────────────────┘└─┘  └─────────┘ └────┘└─┘└┘
doc  ─────┘                   └─┘                       └┘
txt  ─────┘                   └─┘                       └┘
par  ─────┘                   └─┘                       └┘
pid  ─────┘                   └─┘                       └┘
st   ─────────────────────────────────────────────────────────┘
 83  (λ a s has hs ih his, by rw [← set.union_singleton, algebra.adjoin_union_coe_submodule]; exact
id        └─┘ └┘ └┘ └─┘           └─────────────────┘  └────────────────────────────────┘
src                           └────┘└─────────────────┘└┘└────────────────────────────────┘  └─────
typ       └─┘ └┘ └┘ └─┘     └────┘└─────────────────┘└┘└────────────────────────────────┘  └─────
doc                           └────┘                   └┘                                    └─────
txt                           └────┘                   └┘                                    └─────
par                           └────┘                   └┘                                    └─────
pid                             └──┘                   └┘                                         
st                           └────────────────────────┘└──────────────────────────────────┘└───────
 84    fg_mul _ _ (ih $ λ i hi, his i $ set.mem_insert_of_mem a hi)
id     └────┘      └┘                   └───────────────────┘
src  ─┘└────┘└───┘     └─────┘     └───────────────────┘   └─
typ  ─┘└────┘└───┘ └┘  └─────┘     └───────────────────┘   └─
doc  ─┘      └───┘     └─────┘                             └─
txt  ─┘      └───┘     └─────┘                             └─
par  ─┘      └───┘     └─────┘                             └─
pid  ─┘      └───┘     └─────┘                             └─
st   ───────────────────────────────────────────────────────────────
 85      (fg_adjoin_singleton_of_integral _ $ his a $ set.mem_insert a s)) his
id        └─────────────────────────────┘     └─┘     └────────────┘     └─┘
src  ───┘ └─────────────────────────────┘└─┘      └────────────┘  
typ  ───┘ └─────────────────────────────┘└─┘ └─┘  └────────────┘  └─┘
doc  ───┘                                └─┘                      
txt  ───┘                                └─┘                      
par  ───┘                                └─┘                      
pid  ───┘                                └─┘                      
st   ───────────────────────────────────────────────────────────────────┘
 86  
 87  theorem is_integral_of_noetherian' (H : is_noetherian R A) (x : A) :
id                                           └───────────┘         
src                                          └───────────┘
typ                                          └───────────┘         
 88    is_integral R x :=
id     └─────────┘  
src    └─────────┘
typ    └─────────┘  
 89  begin
st   └─────
 90    let leval : @linear_map R (polynomial R) A _ _ _ _ _ := (aeval R A x).to_linear_map,
id                  └────────┘    └────────┘                  └───┘   
src    └──────────┘ └────────┘  └────────┘ └┘ └────────────┘ └───┘   └─────────────┘
typ    └──────────┘ └────────┘  └────────┘└┘└────────────┘ └───┘└─────────────┘
doc    └──────────┘             └────────┘ └┘ └────────────┘ └───┘   └─────────────┘
txt    └──────────┘                        └┘ └────────────┘         └─────────────┘
par    └──────────┘                        └┘ └────────────┘         └─────────────┘
pid    └───────┘└─┘                        └┘ └────────┘└──┘         └────────────┘
st   ────────────────────────────────────────────────────────────────────────────────────┘└─
 91    let D : ℕ → submodule R A := λ n, (degree_le R n).map leval,
id                 └───────┘            └───────┘         └───┘
src    └──────┘  └───────┘  └──┘ └──┘ └───────┘  └────┘
typ    └──────┘  └───────┘└──┘ └──┘ └───────┘ └────┘└───┘
doc    └──────┘  └───────┘  └──┘ └──┘ └───────┘  └────┘
txt    └──────┘             └──┘ └──┘            └────┘
par    └──────┘             └──┘ └──┘            └────┘
pid    └───┘└─┘             └──┘ └──┘            └────┘
st   ────────────────────────────────────────────────────────────┘└─
 92    let M := well_founded.min (is_noetherian_iff_well_founded.1 H)
id              └──────────────┘  └────────────────────────────┘   
src    └───────┘└──────────────┘ └────────────────────────────┘└─┘ └─
typ    └───────┘└──────────────┘ └────────────────────────────┘└─┘└─
doc    └───────┘└──────────────┘                               └─┘ └─
txt    └───────┘                                               └─┘ └─
par    └───────┘                                               └─┘ └─
pid    └───┘└─┘                                               └─┘ └─
st   ─────────────────────────────────────────────────────────────────
 93      (set.range D) ⟨_, ⟨0, rfl⟩⟩,
id        └───────┘           └─┘
src  ───┘ └───────┘ └┘ └─┘ └─┘└─┘└┘
typ  ───┘ └───────┘└┘ └─┘ └─┘└─┘└┘
doc  ───┘ └───────┘ └┘ └─┘ └─┘   └┘
txt  ───┘           └┘ └─┘ └─┘   └┘
par  ───┘           └┘ └─┘ └─┘   └┘
pid  ───┘           └┘ └─┘ └─┘   └┘
st   ──────────────────────────────┘└─
 94    have HM : M ∈ set.range D := well_founded.min_mem _ _ _,
id                 └───────┘     └──────────────────┘
src    └────────┘ └───────┘ └──┘└──────────────────┘└────┘
typ    └────────┘└───────┘└──┘└──────────────────┘└────┘
doc    └────────┘  └───────┘ └──┘                    └────┘
txt    └────────┘            └──┘                    └────┘
par    └────────┘            └──┘                    └────┘
pid    └─────┘└─┘            └──┘                    └────┘
st   ────────────────────────────────────────────────────────┘└─
 95    cases HM with N HN,
id           └┘
src    └────┘  └────────┘
typ    └────┘└┘└────────┘
doc    └────┘  └────────┘
txt    └────┘  └────────┘
par    └────┘  └────────┘
pid           └────────┘
st   ───────────────────┘└─
 96    have HM : ¬M < D (N+1) := well_founded.not_lt_min
id                         └─────────────────────┘
src    └────────┘    └────┘└─────────────────────┘
typ    └────────┘ └────┘└─────────────────────┘
doc    └────────┘       └────┘                       
txt    └────────┘       └────┘                       
par    └────────┘       └────┘                       
pid    └─────┘└─┘       └┘└──┘                       
st   ────────────────────────────────────────────────────
 97      (is_noetherian_iff_well_founded.1 H) (set.range D) _ ⟨N+1, rfl⟩,
id        └────────────────────────────┘      └───────┘          └─┘
src  ───┘ └────────────────────────────┘└─┘ └┘ └───────┘ └──┘   └─┘└─┘
typ  ───┘ └────────────────────────────┘└─┘└┘ └───────┘└──┘  └─┘└─┘
doc  ───┘                               └─┘ └┘ └───────┘ └──┘   └─┘   
txt  ───┘                               └─┘ └┘           └──┘   └─┘   
par  ───┘                               └─┘ └┘           └──┘   └─┘   
pid  ───┘                               └─┘ └┘           └──┘   └─┘   
st   ──────────────────────────────────────────────────────────────────┘└─
 98    rw ← HN at HM,
id          └┘
src    └───┘  └────┘
typ    └───┘└┘└────┘
doc    └───┘  └────┘
txt    └───┘  └────┘
par    └───┘  └────┘
pid      └─┘  └────┘
st   ──────────────┘└─
 99    have HN2 : D (N+1) ≤ D N := classical.by_contradiction (λ H, HM
id                              └────────────────────────┘       └┘
src    └─────────┘    └─┘  └──┘└────────────────────────┘  └──┘  
typ    └─────────┘    └─┘└──┘└────────────────────────┘  └──┘└┘
doc    └─────────┘    └─┘   └──┘                            └──┘  
txt    └─────────┘    └─┘   └──┘                            └──┘  
par    └─────────┘    └─┘   └──┘                            └──┘  
pid    └──────┘└─┘    └─┘   └──┘                            └──┘  
st   ──────────────────────────────────────────────────────────────────
100      (lt_of_le_not_le (map_mono (degree_le_mono
id        └─────────────┘  └──────┘  └────────────┘
src  ───┘ └─────────────┘ └──────┘ └────────────┘
typ  ───┘ └─────────────┘ └──────┘ └────────────┘
doc  ───┘                                        
txt  ───┘                                        
par  ───┘                                        
pid  ───┘                                        
st   ───────────────────────────────────────────────
101        (with_bot.coe_le_coe.2 (nat.le_succ N)))) H)),
id          └─────────────────┘    └─────────┘ 
src  ─────┘ └─────────────────┘└─┘ └─────────┘ └───┘ └┘
typ  ─────┘ └─────────────────┘└─┘ └─────────┘└───┘ └┘
doc  ─────┘                    └─┘             └───┘ └┘
txt  ─────┘                    └─┘             └───┘ └┘
par  ─────┘                    └─┘             └───┘ └┘
pid  ─────┘                    └─┘             └───┘ └┘
st   ──────────────────────────────────────────────────┘└─
102    have HN3 : leval (X^(N+1)) ∈ D N,
id                └───┘            
src    └─────────┘         └──┘  
typ    └─────────┘└───┘    └──┘ 
doc    └─────────┘          └──┘  
txt    └─────────┘           └──┘  
par    └─────────┘           └──┘  
pid    └──────┘└─┘           └──┘  
st   ─────────────────────────────────┘└─
103    { exact HN2 (mem_map_of_mem (mem_degree_le.2 (degree_X_pow_le _))) },
id             └─┘  └────────────┘  └───────────┘    └─────────────┘
src      └────┘    └────────────┘ └───────────┘└─┘ └─────────────┘└────┘
typ      └────┘└─┘ └────────────┘ └───────────┘└─┘ └─────────────┘└────┘
doc      └────┘                                └─┘                └────┘
txt      └────┘                                └─┘                └────┘
par      └────┘                                └─┘                └────┘
pid                                           └─┘                └───┘
st   ───┘└───────────────────────────────────────────────────────────────┘└┘
104    rcases HN3 with ⟨p, hdp, hpe⟩,
id            └─┘
src    └─────┘   └─────────────────┘
typ    └─────┘└─┘└─────────────────┘
doc    └─────┘   └─────────────────┘
txt    └─────┘   └─────────────────┘
par    └─────┘   └─────────────────┘
pid             └─────────────────┘
st   ──────────────────────────────┘
105    refine ⟨X^(N+1) - p, monic_X_pow_sub (mem_degree_le.1 hdp), _⟩,
id                      └─────────────┘  └───────────┘   └─┘
src    └─────┘     └─┘ └┘└─────────────┘ └───────────┘└─┘   └───┘
typ    └─────┘    └─┘└┘└─────────────┘ └───────────┘└─┘└─┘└───┘
doc    └─────┘     └─┘  └┘                             └─┘   └───┘
txt    └─────┘      └─┘  └┘                             └─┘   └───┘
par    └─────┘      └─┘  └┘                             └─┘   └───┘
pid                └─┘  └┘                             └─┘   └───┘
st   ───────────────────────────────────────────────────────────────┘└─
106    show leval (X ^ (N + 1) - p) = 0,
id          └───┘                
src    └───┘          └──┘  └┘└┘
typ    └───┘└───┘    └──┘ └┘└┘
doc    └───┘          └──┘  └┘ └┘
txt    └───┘           └──┘  └┘ └┘
par    └───┘           └──┘  └┘ └┘
pid    └───┘           └──┘  └┘ 
st   ─────────────────────────────────┘└─
107    rw [linear_map.map_sub, hpe, sub_self]
id         └────────────────┘  └─┘  └──────┘
src    └──┘└────────────────┘└┘   └┘└──────┘└┘
typ    └──┘└────────────────┘└┘└─┘└┘└──────┘└┘
doc    └──┘                  └┘   └┘        └┘
txt    └──┘                  └┘   └┘        └┘
par    └──┘                  └┘   └┘        └┘
pid      └┘                  └┘   └┘        
st   ───────────────────────┘└───┘└────────┘
108  end
st   └─┘
109  
110  theorem is_integral_of_noetherian (S : subalgebra R A)
id                                          └────────┘  
src                                         └────────┘
typ                                         └────────┘  
111    (H : is_noetherian R (S : submodule R A)) (x : A) (hx : x ∈ S) :
id          └───────────┘      └───────┘                    
src         └───────────┘        └───────┘                       
typ         └───────────┘      └───────┘                    
doc                              └───────┘
112    is_integral R x :=
id     └─────────┘  
src    └─────────┘
typ    └─────────┘  
113  begin
st   └─────
114    letI : algebra R S := S.algebra,
id            └─────┘      └───────┘
src    └─────┘└─────┘  └──┘└───────┘
typ    └─────┘└─────┘└──┘└───────┘
doc    └─────┘└─────┘  └──┘
txt    └─────┘         └──┘
par    └─────┘         └──┘
pid        └┘         └──┘
st   ────────────────────────────────┘└─
115    letI : comm_ring S := S.comm_ring R A,
id            └───────┘     └─────────┘  
src    └─────┘└───────┘ └──┘└─────────┘ 
typ    └─────┘└───────┘└──┘└─────────┘
doc    └─────┘          └──┘            
txt    └─────┘          └──┘            
par    └─────┘          └──┘            
pid        └┘          └──┘            
st   ──────────────────────────────────────┘└─
116    suffices : is_integral R (⟨x, hx⟩ : S),
id                └─────────┘      └┘    
src    └─────────┘└─────────┘    └┘  └──┘ 
typ    └─────────┘└─────────┘  └┘└┘└──┘
doc    └─────────┘               └┘  └──┘ 
txt    └─────────┘               └┘  └──┘ 
par    └─────────┘               └┘  └──┘ 
pid    └───────┘└┘               └┘  └──┘ 
st   ───────────────────────────────────────┘└─
117    { rcases this with ⟨p, hpm, hpx⟩,
id              └──┘
src      └─────┘    └─────────────────┘
typ      └─────┘└──┘└─────────────────┘
doc      └─────┘    └─────────────────┘
txt      └─────┘    └─────────────────┘
par      └─────┘    └─────────────────┘
pid                └─────────────────┘
st   ───┘└────────────────────────────┘└─
118      replace hpx := congr_arg subtype.val hpx,
id                      └───────┘ └─────────┘ └─┘
src      └─────────────┘└───────┘└─────────┘
typ      └─────────────┘└───────┘└─────────┘└─┘
doc      └─────────────┘                    
txt      └─────────────┘                    
par      └─────────────┘                    
pid             └──┘└─┘                    
st   ───────────────────────────────────────────┘└─
119      refine ⟨p, hpm, eq.trans _ hpx⟩,
id                 └─┘  └──────┘   └─┘
src      └─────┘  └┘   └┘└──────┘└─┘   
typ      └─────┘ └┘└─┘└┘└──────┘└─┘└─┘
doc      └─────┘  └┘   └┘        └─┘   
txt      └─────┘  └┘   └┘        └─┘   
par      └─────┘  └┘   └┘        └─┘   
pid              └┘   └┘        └─┘   
st   ──────────────────────────────────┘└─
120      simp only [aeval_def, eval₂, finsupp.sum],
id                  └───────┘  └───┘  └─────────┘
src      └─────────┘└───────┘└┘└───┘└┘└─────────┘
typ      └─────────┘└───────┘└┘└───┘└┘└─────────┘
doc      └─────────┘         └┘└───┘└┘└─────────┘
txt      └─────────┘         └┘     └┘           
par      └─────────┘         └┘     └┘           
pid          └──┘└┘         └┘     └┘           
st   ────────────────────────────────────────────┘└─
121      rw ← p.support.sum_hom subtype.val,
id            └───────────────┘ └─────────┘
src      └───┘└───────────────┘└─────────┘
typ      └───┘└───────────────┘└─────────┘
doc      └───┘                 
txt      └───┘                 
par      └───┘                 
pid        └─┘                 
st   ─────────────────────────────────────┘└─
122      { refine finset.sum_congr rfl (λ n hn, _),
id                └──────────────┘ └─┘
src        └─────┘└──────────────┘└─┘  └───────┘
typ        └─────┘└──────────────┘└─┘  └───────┘
doc        └─────┘                     └───────┘
txt        └─────┘                     └───────┘
par        └─────┘                     └───────┘
pid                                   └───────┘
st   ─────┘└─────────────────────────────────────┘└─
123        change _ = _ * _,
id                     
src        └───────┘└─┘└┘
typ        └───────┘└─┘└┘
doc        └───────┘ └─┘ └┘
txt        └───────┘ └─┘ └┘
par        └───────┘ └─┘ └┘
pid              └─┘ └─┘ └┘
st   ─────────────────────┘└─
124        rw is_semiring_hom.map_pow subtype.val, refl,
id            └─────────────────────┘ └─────────┘
src        └─┘└─────────────────────┘└─────────┘  └──┘
typ        └─┘└─────────────────────┘└─────────┘  └──┘
doc        └─┘                                    └──┘
txt        └─┘                                    └──┘
par        └─┘                                    └──┘
pid                                 
st   ───────────────────────────────────────────┘└────┘└─
125        split; intros; refl },
src        └───┘  └────┘  └───┘
typ        └───┘  └────┘  └───┘
doc        └───┘  └────┘  └───┘
txt        └───┘  └────┘  └───┘
par        └───┘  └────┘  └───┘
pid                           
st   ─────────────────────────┘└┘
126      refine { map_add := _, map_zero := _ }; intros; refl },
src      └─────┘ └────────────────────────────┘  └────┘  └───┘
typ      └─────┘ └────────────────────────────┘  └────┘  └───┘
doc      └─────┘ └────────────────────────────┘  └────┘  └───┘
txt      └─────┘ └────────────────────────────┘  └────┘  └───┘
par      └─────┘ └────────────────────────────┘  └────┘  └───┘
pid             └────────────────────────────┘              
st   ────────────────────────────────────────────────────────┘└┘
127    refine is_integral_of_noetherian' H ⟨x, hx⟩
id            └────────────────────────┘     └┘
src    └─────┘└────────────────────────┘   └┘  └┘
typ    └─────┘└────────────────────────┘ └┘└┘└┘
doc    └─────┘                             └┘  └┘
txt    └─────┘                             └┘  └┘
par    └─────┘                             └┘  └┘
pid                                       └┘  
st   ─────────────────────────────────────────────┘
128  end
st   └─┘
129  
130  set_option class.instance_max_depth 100
doc             └──────────────────────┘
131  theorem is_integral_of_mem_of_fg (S : subalgebra R A)
id                                         └────────┘  
src                                        └────────┘
typ                                        └────────┘  
132    (HS : (S : submodule R A).fg) (x : A) (hx : x ∈ S) : is_integral R x :=
id               └───────┘   └┘                      └─────────┘  
src               └───────┘     └┘                         └─────────┘
typ              └───────┘   └┘                      └─────────┘  
doc               └───────┘
133  begin
st   └─────
134    cases HS with y hy,
id           └┘
src    └────┘  └────────┘
typ    └────┘└┘└────────┘
doc    └────┘  └────────┘
txt    └────┘  └────────┘
par    └────┘  └────────┘
pid           └────────┘
st   ───────────────────┘└─
135    obtain ⟨lx, hlx1, hlx2⟩ :
src    └─────────────────────────
typ    └─────────────────────────
doc    └─────────────────────────
txt    └─────────────────────────
par    └─────────────────────────
pid          └───────────────────
st   ────────────────────────────
136      ∃ (l : A →₀ R) (H : l ∈ finsupp.supported R R ↑y), (finsupp.total A A R id) l = x,
id               └┘            └───────────────┘        └───────────┘     └┘     
src  ───┘└────┘ └┘ └─────┘ └───────────────┘    └───────────┘   └┘└┘ 
typ  ───┘└────┘ └┘ └─────┘ └───────────────┘   └───────────┘ └┘└┘ 
doc  ───┘ └────┘ └┘ └─────┘                         └───────────┘     └┘  
txt  ───┘ └────┘    └─────┘                                           └┘  
par  ───┘ └────┘    └─────┘                                           └┘  
pid  ───┘ └────┘    └─────┘                                           └┘  
st   ────────────────────────────────────────────────────────────────────────────────────┘└─
137    { rwa [←(@finsupp.mem_span_iff_total A A R _ _ _ id ↑y x), set.image_id ↑y, hy] },
id               └────────────────────────┘           └┘      └──────────┘    └┘
src      └────┘  └────────────────────────┘   └─────┘└┘   └─┘└──────────┘  └┘  └┘
typ      └────┘  └────────────────────────┘ └─────┘└┘ └─┘└──────────┘ └┘└┘└┘
doc      └────┘                               └─────┘     └─┘              └┘  └┘
txt      └────┘                               └─────┘     └─┘              └┘  └┘
par      └────┘                               └─────┘     └─┘              └┘  └┘
pid         └─┘                               └─────┘     └─┘              └┘  
st   ───┘└─────────────────────────────────────────────────────┘└───────────────┘└──┘└┘
138    have : ∀ (jk : (↑(y.product y) : set (A × A))), jk.1.1 * jk.1.2 ∈ (span R ↑y : submodule R A),
id                      └───────┘      └─┘                             └──┘      └───────┘   
src    └─────┘ └─────┘   └───────┘ └──┘└─┘   └─┘   └───┘  └───┘  └──┘   └─┘└───────┘  
typ    └─────┘ └─────┘  └───────┘ └──┘└─┘   └─┘   └───┘  └───┘  └──┘ └─┘└───────┘ 
doc    └─────┘ └─────┘   └───────┘ └──┘       └─┘   └───┘   └───┘  └──┘   └─┘└───────┘  
txt    └─────┘ └─────┘             └──┘       └─┘   └───┘   └───┘         └─┘           
par    └─────┘ └─────┘             └──┘       └─┘   └───┘   └───┘         └─┘           
pid    └───┘└┘ └─────┘             └──┘       └─┘   └───┘   └───┘         └─┘           
st   ──────────────────────────────────────────────────────────────────────────────────────────────┘└─
139    { intros jk,
src      └───────┘
typ      └───────┘
doc      └───────┘
txt      └───────┘
par      └───────┘
pid            └─┘
st   ───┘└───────┘└─
140      let j : ↥(↑y : set A) := ⟨jk.1.1, (finset.mem_product.1 jk.2).1⟩,
id                    └─┘                └────────────────┘   └┘
src      └──────┘   └─┘└─┘ └───┘   └────┘ └────────────────┘└─┘  └────┘
typ      └──────┘  └─┘└─┘└───┘   └────┘ └────────────────┘└─┘└┘└────┘
doc      └──────┘    └─┘    └───┘   └────┘                   └─┘  └────┘
txt      └──────┘    └─┘    └───┘   └────┘                   └─┘  └────┘
par      └──────┘    └─┘    └───┘   └────┘                   └─┘  └────┘
pid      └───┘└─┘    └─┘    └──┘   └────┘                   └─┘  └────┘
st   ───────────────────────────────────────────────────────────────────┘└─
141      let k : ↥(↑y : set A) := ⟨jk.1.2, (finset.mem_product.1 jk.2).2⟩,
id                     └─┘                └────────────────┘   └┘
src      └──────┘    └─┘└─┘ └───┘   └────┘ └────────────────┘└─┘  └────┘
typ      └──────┘   └─┘└─┘└───┘   └────┘ └────────────────┘└─┘└┘└────┘
doc      └──────┘    └─┘    └───┘   └────┘                   └─┘  └────┘
txt      └──────┘    └─┘    └───┘   └────┘                   └─┘  └────┘
par      └──────┘    └─┘    └───┘   └────┘                   └─┘  └────┘
pid      └───┘└─┘    └─┘    └──┘   └────┘                   └─┘  └────┘
st   ───────────────────────────────────────────────────────────────────┘└─
142      have hj : j.1 ∈ (span R ↑y : submodule R A) := subset_span j.2,
id                       └──┘      └───────┘        └─────────┘ 
src      └────────┘ └─┘  └──┘   └─┘└───────┘  └───┘└─────────┘ └┘
typ      └────────┘└─┘  └──┘ └─┘└───────┘ └───┘└─────────┘└┘
doc      └────────┘ └─┘  └──┘   └─┘└───────┘  └───┘            └┘
txt      └────────┘ └─┘         └─┘           └───┘            └┘
par      └────────┘ └─┘         └─┘           └───┘            └┘
pid      └─────┘└─┘ └─┘         └─┘           └──┘            └┘
st   ─────────────────────────────────────────────────────────────────┘└─
143      have hk : k.1 ∈ (span R ↑y : submodule R A) := subset_span k.2,
id                       └──┘      └───────┘        └─────────┘ 
src      └────────┘ └─┘  └──┘   └─┘└───────┘  └───┘└─────────┘ └┘
typ      └────────┘└─┘  └──┘ └─┘└───────┘ └───┘└─────────┘└┘
doc      └────────┘ └─┘  └──┘   └─┘└───────┘  └───┘            └┘
txt      └────────┘ └─┘         └─┘           └───┘            └┘
par      └────────┘ └─┘         └─┘           └───┘            └┘
pid      └─────┘└─┘ └─┘         └─┘           └──┘            └┘
st   ─────────────────────────────────────────────────────────────────┘└─
144      revert hj hk, rw hy, exact @is_submonoid.mul_mem A _ S _ j.1 k.1 },
id                        └┘         └──────────────────┘          
src      └──────────┘  └─┘    └────┘ └──────────────────┘ └─┘ └─┘ └─┘ └─┘
typ      └──────────┘  └─┘└┘  └────┘ └──────────────────┘└─┘└─┘└─┘└─┘
doc      └──────────┘  └─┘    └────┘                      └─┘ └─┘ └─┘ └─┘
txt      └──────────┘  └─┘    └────┘                      └─┘ └─┘ └─┘ └─┘
par      └──────────┘  └─┘    └────┘                      └─┘ └─┘ └─┘ └─┘
pid            └────┘                                   └─┘ └─┘ └─┘ └─┘
st   ───────────────┘└─────┘└────────────────────────────────────────────┘└┘
145    rw ← set.image_id ↑y at this,
id          └──────────┘  
src    └───┘└──────────┘  └──────┘
typ    └───┘└──────────┘ └──────┘
doc    └───┘              └──────┘
txt    └───┘              └──────┘
par    └───┘              └──────┘
pid      └─┘              └──────┘
st   ─────────────────────────────┘└─
146    simp only [finsupp.mem_span_iff_total] at this,
id                └────────────────────────┘
src    └─────────┘└────────────────────────┘└───────┘
typ    └─────────┘└────────────────────────┘└───────┘
doc    └─────────┘                          └───────┘
txt    └─────────┘                          └───────┘
par    └─────────┘                          └───────┘
pid        └──┘└┘                          └─────┘
st   ───────────────────────────────────────────────┘└─
147    choose ly hly1 hly2,
src    └─────────────────┘
typ    └─────────────────┘
doc    └─────────────────┘
txt    └─────────────────┘
par    └─────────────────┘
pid          └─┘└────────┘
st   ────────────────────┘└─
148    let S₀' : finset R := lx.frange ∪ finset.bind finset.univ (finsupp.frange ∘ ly),
id               └────┘     └───────┘  └─────────┘ └─────────┘  └────────────┘  └┘
src    └────────┘└────┘ └──┘└───────┘└─────────┘└─────────┘ └────────────┘  
typ    └────────┘└────┘└──┘└───────┘└─────────┘└─────────┘ └────────────┘└┘
doc    └────────┘└────┘ └──┘          └─────────┘└─────────┘                  
txt    └────────┘       └──┘                                                  
par    └────────┘       └──┘                                                  
pid    └─────┘└─┘       └──┘                                                  
st   ────────────────────────────────────────────────────────────────────────────────┘└─
149    let S₀ : set R := ring.closure ↑S₀',
id              └─┘     └──────────┘  └─┘
src    └───────┘└─┘ └──┘└──────────┘
typ    └───────┘└─┘└──┘└──────────┘ └─┘
doc    └───────┘    └──┘            
txt    └───────┘    └──┘            
par    └───────┘    └──┘            
pid    └────┘└─┘    └──┘            
st   ────────────────────────────────────┘└─
150    refine is_integral_of_subring (ring.closure ↑S₀') _,
id            └────────────────────┘  └──────────┘  └─┘
src    └─────┘└────────────────────┘ └──────────┘    └─┘
typ    └─────┘└────────────────────┘ └──────────┘ └─┘└─┘
doc    └─────┘                                       └─┘
txt    └─────┘                                       └─┘
par    └─────┘                                       └─┘
pid                                                 └─┘
st   ────────────────────────────────────────────────────┘└─
151    letI : algebra S₀ (algebra.comap S₀ R A) := algebra.comap.algebra _ _ _,
id            └─────┘     └───────────┘ └┘       └───────────────────┘
src    └─────┘└─────┘   └───────────┘    └───┘└───────────────────┘└────┘
typ    └─────┘└─────┘   └───────────┘└┘└───┘└───────────────────┘└────┘
doc    └─────┘└─────┘   └───────────┘    └───┘└───────────────────┘└────┘
txt    └─────┘                           └───┘                     └────┘
par    └─────┘                           └───┘                     └────┘
pid        └┘                           └──┘                     └────┘
st   ────────────────────────────────────────────────────────────────────────┘└─
152    letI hmod : module S₀ (algebra.comap S₀ R A) := algebra.to_module,
id                 └────┘     └───────────┘ └┘       └───────────────┘
src    └──────────┘└────┘   └───────────┘    └───┘└───────────────┘
typ    └──────────┘└────┘   └───────────┘└┘└───┘└───────────────┘
doc    └──────────┘└────┘   └───────────┘    └───┘
txt    └──────────┘                          └───┘
par    └──────────┘                          └───┘
pid        └───┘└─┘                          └──┘
st   ──────────────────────────────────────────────────────────────────┘└─
153    have : (span S₀ (insert 1 (↑y:set A) : set (algebra.comap S₀ R A)) : submodule S₀ (algebra.comap S₀ R A)) =
id             └──┘     └────┘                                              └───────┘
src    └─────┘ └──┘   └────┘└─┘       └──┘                     └───┘└───────┘                    └─┘ 
typ    └─────┘ └──┘   └────┘└─┘       └──┘                     └───┘└───────┘                    └─┘ 
doc    └─────┘ └──┘         └─┘       └──┘                     └───┘└───────┘                    └─┘ 
txt    └─────┘              └─┘       └──┘                     └───┘                             └─┘ 
par    └─────┘              └─┘       └──┘                     └───┘                             └─┘ 
pid    └───┘└┘              └─┘       └──┘                     └───┘                             └─┘ 
st   ──────────────────────────────────────────────────────────────────────────────────────────────────────────────
154        (algebra.adjoin S₀ ((↑y : set A) : set (algebra.comap S₀ R A)) : subalgebra S₀ (algebra.comap S₀ R A)),
id          └────────────┘          └─┘          └───────────┘ └┘        └────────┘
src  ─────┘ └────────────┘      └─┘└─┘ └──┘    └───────────┘    └───┘└────────┘                    └┘
typ  ─────┘ └────────────┘     └─┘└─┘└──┘    └───────────┘└┘ └───┘└────────┘                    └┘
doc  ─────┘                     └─┘    └──┘    └───────────┘    └───┘                              └┘
txt  ─────┘                     └─┘    └──┘                     └───┘                              └┘
par  ─────┘                     └─┘    └──┘                     └───┘                              └┘
pid  ─────┘                     └─┘    └──┘                     └───┘                              └┘
st   ───────────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
155    { apply le_antisymm,
id             └─────────┘
src      └────┘└─────────┘
typ      └────┘└─────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───┘└───────────────┘└─
156      { rw [span_le, set.insert_subset, mem_coe], split,
id             └─────┘  └───────────────┘
src        └──┘└─────┘└┘└───────────────┘
typ        └──┘└─────┘└┘└───────────────┘
doc        └──┘       └┘
txt        └──┘       └┘
par        └──┘       └┘
pid          └┘       └┘
st   ─────┘└─────────┘└─────────────────┘
157        change _ ∈ ring.closure _, exact is_submonoid.one_mem _, exact algebra.subset_adjoin },
st                                                                                              └┘
158      rw [algebra.adjoin_eq_span, span_le], intros r hr, refine monoid.in_closure.rec_on hr _ _ _,
159      { intros r hr, exact subset_span (set.mem_insert_of_mem _ hr) },
st                                                                     └┘
160      { exact subset_span (set.mem_insert _ _) },
st                                                └┘
161      intros r1 r2 hr1 hr2 ih1 ih2,
162      rw ← set.image_id (insert _ ↑y) at ih1 ih2,
id                                    
typ                                   
163      simp only [mem_coe, finsupp.mem_span_iff_total] at ih1 ih2,
164      have ih1' := ih1, have ih2' := ih2,
165      rcases ih1' with ⟨l1, hl1, rfl⟩, rcases ih2' with ⟨l2, hl2, rfl⟩,
166      simp only [finsupp.total_apply, finsupp.sum_mul, finsupp.mul_sum, mem_coe],
167      rw [finsupp.sum], refine sum_mem _ _, intros r2 hr2,
168      rw [finsupp.sum], refine sum_mem _ _, intros r1 hr1,
169      rw [algebra.mul_smul_comm, algebra.smul_mul_assoc],
170      letI : module ↥S₀ A := hmod, refine smul_mem _ _ (smul_mem _ _ _),
id                      └┘ 
typ                     └┘ 
171      rcases hl1 hr1 with rfl | hr1,
172      { change 1 * r2 ∈ _, rw one_mul r2, exact subset_span (hl2 hr2) },
st                                                                       └┘
173      rcases hl2 hr2 with rfl | hr2,
174      { change r1 * 1 ∈ _, rw mul_one, exact subset_span (set.mem_insert_of_mem _ hr1) },
st                                                                                        └┘
175      let jk : ↥(↑(finset.product y y) : set (A × A)) := ⟨(r1, r2), finset.mem_product.2 ⟨hr1, hr2⟩⟩,
id                                         └─┘      
src                                         └─┘
typ                                        └─┘      
176      specialize hly2 jk, change _ = r1 * r2 at hly2, rw [id, id, ← hly2, finsupp.total_apply],
177      rw [finsupp.sum], refine sum_mem _ _, intros z hz,
178      have : ly jk z ∈ S₀,
id                       └┘
typ                      └┘
179      { apply ring.subset_closure,
180        apply finset.mem_union_right, apply finset.mem_bind.2,
181        exact ⟨jk, finset.mem_univ _, by convert finset.mem_image_of_mem _ hz⟩ },
st                                                                                └┘
182      change @has_scalar.smul S₀ (algebra.comap S₀ R A) hmod.to_has_scalar ⟨ly jk z, this⟩ z ∈ _,
id                                                 └┘                                       
typ                                                └┘                                       
183      exact smul_mem _ _ (subset_span (set.mem_insert_of_mem _ (hly1 _ hz))) },
st                                                                              └┘
184    haveI : is_noetherian_ring ↥S₀ :=
id                                 └┘
typ                                └┘
185    by { convert is_noetherian_ring_closure _ (finset.finite_to_set _), apply_instance },
st                                                                                        └┘
186    apply is_integral_of_noetherian
187      (algebra.adjoin S₀ ((↑y : set A) : set (algebra.comap S₀ R A)) : subalgebra S₀ (algebra.comap S₀ R A))
id                                 └─┘                           
src                                └─┘
typ                                └─┘                           
188      (is_noetherian_of_fg_of_noetherian _ ⟨insert 1 y, by rw finset.coe_insert; convert this⟩),
id                                                      
typ                                                     
189    show x ∈ ((algebra.adjoin S₀ ((↑y : set A) : set (algebra.comap S₀ R A)) :
id                                       └─┘                           
src                                        └─┘
typ                                      └─┘                           
190        subalgebra S₀ (algebra.comap S₀ R A)) : submodule S₀ (algebra.comap S₀ R A)),
191    rw [← hlx2, finsupp.total_apply, finsupp.sum], refine sum_mem _ _, intros r hr,
192    rw ← this,
193    have : lx r ∈ ring.closure ↑S₀' :=
id                                └─┘
typ                               └─┘
194      ring.subset_closure (finset.mem_union_left _ (by convert finset.mem_image_of_mem _ hr)),
195    change @has_scalar.smul S₀ (algebra.comap S₀ R A) hmod.to_has_scalar ⟨lx r, this⟩ r ∈ _,
id                                               └┘                                    
typ                                              └┘                                    
196    rw finsupp.mem_supported at hlx1,
197    exact smul_mem _ _ (subset_span (set.mem_insert_of_mem _ (hlx1 hr))),
198  end
st   └─┘
199  
200  theorem is_integral_of_mem_closure {x y z : A}
id                                               
typ                                              
201    (hx : is_integral R x) (hy : is_integral R y)
id                                             
typ                                            
202    (hz : z ∈ ring.closure ({x, y} : set A)) :
id                                     
src                                       
typ                                    
203    is_integral R z :=
id                  
typ                 
204  begin
205    have := fg_mul _ _ (fg_adjoin_singleton_of_integral x hx) (fg_adjoin_singleton_of_integral y hy),
id                                                                                               
typ                                                                                              
206    rw [← algebra.adjoin_union_coe_submodule, set.union_singleton, insert] at this,
207    exact is_integral_of_mem_of_fg (algebra.adjoin R {x, y}) this z
id                                                                
typ                                                               
208      (ring.closure_mono (set.subset_union_right _ _) hz)
209  end
st   └─┘
210  
211  theorem is_integral_zero : is_integral R (0:A) :=
id                                              
typ                                             
212  algebra.map_zero R A ▸ is_integral_algebra_map
id                     
typ                    
213  
214  theorem is_integral_one : is_integral R (1:A) :=
id                                             
typ                                            
215  algebra.map_one R A ▸ is_integral_algebra_map
id                    
typ                   
216  
217  theorem is_integral_add {x y : A}
id                                  
typ                                 
218    (hx : is_integral R x) (hy : is_integral R y) :
id                                             
typ                                            
219    is_integral R (x + y) :=
id                      
typ                     
220  is_integral_of_mem_closure hx hy (is_add_submonoid.add_mem
221    (ring.subset_closure (or.inr (or.inl rfl))) (ring.subset_closure (or.inl rfl)))
222  
223  theorem is_integral_neg {x : A}
id                                
typ                               
224    (hx : is_integral R x) : is_integral R (-x) :=
id                                           
typ                                          
225  is_integral_of_mem_closure hx hx (is_add_subgroup.neg_mem
226    (ring.subset_closure (or.inl rfl)))
227  
228  theorem is_integral_sub {x y : A}
id                                  
typ                                 
229    (hx : is_integral R x) (hy : is_integral R y) : is_integral R (x - y) :=
id                                                                  
typ                                                                 
230  is_integral_add hx (is_integral_neg hy)
231  
232  theorem is_integral_mul {x y : A}
233    (hx : is_integral R x) (hy : is_integral R y) :
id                                             
typ                                            
234    is_integral R (x * y) :=
id                      
typ                     
235  is_integral_of_mem_closure hx hy (is_submonoid.mul_mem
236    (ring.subset_closure (or.inr (or.inl rfl))) (ring.subset_closure (or.inl rfl)))
237  
238  variables (R A)
239  def integral_closure : subalgebra R A :=
id                                      
typ                                     
240  { carrier := { r | is_integral R r },
id                                  
typ                                 
241    subring :=
242    { zero_mem := is_integral_zero,
243      one_mem := is_integral_one,
244      add_mem := λ _ _, is_integral_add,
id                     
typ                    
245      neg_mem := λ _, is_integral_neg,
id                    
typ                   
246      mul_mem := λ _ _, is_integral_mul },
id                     
typ                    
247    range_le' := λ y ⟨x, hx⟩, hx ▸ is_integral_algebra_map }
id                                  └─────────────────────┘
src                                  └─────────────────────┘
typ                                 └─────────────────────┘
248  
249  theorem mem_integral_closure_iff_mem_fg {r : A} :
id                                                
typ                                               
250    r ∈ integral_closure R A ↔ ∃ M : subalgebra R A, (M : submodule R A).fg ∧ r ∈ M :=
id       └──────────────┘         └────────┘       └───────┘   └┘     
src       └──────────────┘           └────────┘          └───────┘     └┘     
typ      └──────────────┘         └────────┘       └───────┘   └┘     
doc                                                          └───────┘
251  ⟨λ hr, ⟨algebra.adjoin R {r}, fg_adjoin_singleton_of_integral _ hr, algebra.subset_adjoin (or.inl rfl)⟩,
id      └┘   └────────────┘     └─────────────────────────────┘   └┘  └───────────────────┘  └────┘ └─┘
src          └────────────┘       └─────────────────────────────┘       └───────────────────┘  └────┘ └─┘
typ     └┘   └────────────┘     └─────────────────────────────┘   └┘  └───────────────────┘  └────┘ └─┘
252  λ ⟨M, Hf, hrM⟩, is_integral_of_mem_of_fg M Hf _ hrM⟩
id       └┘  └─┘   └──────────────────────┘
src                  └──────────────────────┘
typ      └┘  └─┘   └──────────────────────┘
253  
254  theorem integral_closure_idem : integral_closure (integral_closure R A : set A) A = ⊥ :=
id                                   └──────────────┘  └──────────────┘     └─┘     
src                                  └──────────────┘  └──────────────┘       └─┘       
typ                                  └──────────────┘  └──────────────┘     └─┘     
255  begin
st   └─────
256    rw lattice.eq_bot_iff, intros r hr,
id        └────────────────┘
src    └─┘└────────────────┘
typ    └─┘└────────────────┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ──────────────────────┘
257    rcases is_integral_iff_is_integral_closure_finite.1 hr with ⟨s, hfs, hr⟩,
258    apply algebra.mem_bot.2, refine ⟨⟨_, _⟩, rfl⟩,
259    refine (mem_integral_closure_iff_mem_fg _ _).2 ⟨algebra.adjoin _ (subtype.val '' s ∪ {r}),
id                                                                                           
typ                                                                                          
260      algebra.fg_trans
261        (fg_adjoin_of_finite (set.finite_image _ hfs)
262          (λ y ⟨x, hx, hxy⟩, hxy ▸ x.2))
id              
typ             
263        _,
264      algebra.subset_adjoin (or.inr (or.inl rfl))⟩,
265    refine fg_adjoin_singleton_of_integral _ _,
266    rcases hr with ⟨p, hmp, hpx⟩,
267    refine ⟨to_subring (of_subring _ (of_subring _ p)) _ _, _, hpx⟩,
268    { intros x hx, rcases finsupp.mem_frange.1 hx with ⟨h1, n, rfl⟩,
269      change (coeff p n).1.1 ∈ ring.closure _,
id                       
typ                      
270      rcases ring.exists_list_of_mem_closure (coeff p n).2 with ⟨L, HL1, HL2⟩, rw ← HL2,
id                                                       
typ                                                      
271      clear HL2 hfs h1 hx n hmp hpx hr r p,
272      induction L with hd tl ih, { exact is_add_submonoid.zero_mem _ },
st                                                                      └┘
273      rw list.forall_mem_cons at HL1,
274      rw [list.map_cons, list.sum_cons],
275      refine is_add_submonoid.add_mem _ (ih HL1.2),
276      cases HL1 with HL HL', clear HL' ih tl,
277      induction hd with hd tl ih, { exact is_submonoid.one_mem _ },
st                                                                  └┘
278      rw list.forall_mem_cons at HL,
279      rw list.prod_cons,
280      refine is_submonoid.mul_mem _ (ih HL.2),
281      rcases HL.1 with hs | rfl,
282      { exact algebra.subset_adjoin (set.mem_image_of_mem _ hs) },
st                                                                 └┘
283      exact is_add_subgroup.neg_mem (is_submonoid.one_mem _) },
st                                                              └┘
284    replace hmp := congr_arg subtype.val hmp,
285    replace hmp := congr_arg subtype.val hmp,
286    exact subtype.eq hmp
287  end
st   └─┘
288  
289  end
290  
291  section algebra
292  open algebra
293  variables {R : Type*} {A : Type*} {B : Type*}
294  variables [comm_ring R] [comm_ring A] [comm_ring B]
id              └───────┘     └───────┘     └───────┘
src             └───────┘     └───────┘     └───────┘
typ             └───────┘     └───────┘     └───────┘
295  variables [algebra R A] [algebra A B]
id              └─────┘       └─────┘
src             └─────┘       └─────┘
typ             └─────┘       └─────┘
doc             └─────┘       └─────┘
296  
297  set_option class.instance_max_depth 50
doc             └──────────────────────┘
298  
299  lemma is_integral_trans_aux (x : B) {p : polynomial A} (pmonic : monic p) (hp : aeval A B x p = 0)
id                                           └────────┘             └───┘         └───┘     
src                                           └────────┘              └───┘          └───┘         
typ                                          └────────┘             └───┘         └───┘     
doc                                           └────────┘              └───┘          └───┘
300    (S : set (comap R A B))
id          └─┘  └───┘   
src         └─┘  └───┘
typ         └─┘  └───┘   
doc              └───┘
301    (hS : S = (↑((finset.range (p.nat_degree + 1)).image
id                └──────────┘  └─────────┘     └───┘
src                └──────────┘   └─────────┘     └───┘
typ               └──────────┘  └─────────┘     └───┘
doc                  └──────────┘   └─────────┘      └───┘
302      (λ i, to_comap R A B (p.coeff i))) : set (comap R A B))) :
id            └──────┘     └────┘       └─┘  └───┘   
src            └──────┘         └────┘        └─┘  └───┘
typ           └──────┘     └────┘       └─┘  └───┘   
doc                             └────┘             └───┘
303    is_integral (adjoin R S) (comap.to_comap R A B x) :=
id     └─────────┘  └────┘     └────────────┘    
src    └─────────┘  └────┘       └────────────┘
typ    └─────────┘  └────┘     └────────────┘    
304  begin
st   └─────
305    have coeffs_mem : ∀ i, coeff (map (to_comap R A B) p) i ∈ adjoin R S,
id                            └───┘  └─┘  └──────┘           └────┘  
src    └────────────────┘ └┘ └───┘ └─┘ └──────┘   └┘ └┘ └────┘ 
typ    └────────────────┘ └┘ └───┘ └─┘ └──────┘ └┘└┘ └────┘
doc    └────────────────┘ └┘ └───┘ └─┘            └┘ └┘         
txt    └────────────────┘ └┘                      └┘ └┘         
par    └────────────────┘ └┘                      └┘ └┘         
pid    └─────────────┘└─┘ └┘                      └┘ └┘         
st   ─────────────────────────────────────────────────────────────────────┘
306    { intro i,
src      └─────┘
typ      └─────┘
doc      └─────┘
txt      └─────┘
par      └─────┘
pid           └┘
st       └─────┘└─
307      by_cases hi : i ∈ finset.range (p.nat_degree + 1),
id                        └──────────┘  └──────────┘ 
src      └───────┘  └─┘  └──────────┘ └──────────┘└─┘
typ      └───────┘  └─┘ └──────────┘ └──────────┘└─┘
doc      └───────┘  └─┘  └──────────┘ └──────────┘ └─┘
txt      └───────┘  └─┘                            └─┘
par      └───────┘  └─┘                            └─┘
pid                └─┘                            └─┘
st   ────────────────────────────────────────────────────┘
308      { apply algebra.subset_adjoin, subst S,
309        rw [finset.mem_coe, finset.mem_image, coeff_map],
310        exact ⟨i, hi, rfl⟩ },
id                
typ               
st                            └┘
311      { rw [finset.mem_range, not_lt] at hi,
312        rw [coeff_map, coeff_eq_zero_of_nat_degree_lt hi, alg_hom.map_zero],
313        exact submodule.zero_mem (adjoin R S : submodule R (comap R A B)) } },
id                                                                     
typ                                                                    
st                                                                           └──┘
314    obtain ⟨q, hq⟩ : ∃ q : polynomial (adjoin R S), q.map (algebra_map (comap R A B)) =
315        (p.map $ to_comap R A B),
id                             
typ                            
316    { rw [← set.mem_range], dsimp only,
317      apply (polynomial.mem_map_range _).2,
318      { intros i, specialize coeffs_mem i, rw ← subalgebra.mem_coe at coeffs_mem,
id                                         
typ                                        
319        convert coeffs_mem, exact subtype.val_range },
st                                                     └┘
320      { apply is_ring_hom.is_semiring_hom } },
st                                           └──┘
321    use q,
322    split,
323    { suffices h : (q.map (algebra_map (comap R A B))).monic,
id                                                 
typ                                                
324      { refine @monic_of_injective _ _ _ _ _
325          (by exact is_ring_hom.is_semiring_hom _) _ _ h,
326        exact subtype.val_injective },
st                                     └┘
327      { rw hq, exact monic_map _ pmonic } },
id                                     └┘
typ                                    └┘
st                                         └──┘
328    { convert hp using 1,
329      replace hq := congr_arg (eval (comap.to_comap R A B x)) hq,
id                                 └─────────┘    
src                                └─────────┘
typ                                └─────────┘    
doc                                 
330      convert hq using 1; symmetry, swap,
id                           └──────┘
src                          └──────┘
typ                          └──────┘
doc                          └──────┘
331      exact eval_map _ _,
id             └──────┘
src            └──────┘
typ            └──────┘
332      refine @eval_map _ _ _ _ _ _ (by exact is_ring_hom.is_semiring_hom _) _ },
id               └──────┘                       └─────────────────────────┘
src              └──────┘                       └─────────────────────────┘
typ              └──────┘                       └─────────────────────────┘
doc                                             └─────────────────────────┘
st                                                                               └┘
333  end
st   └─┘
334  
335  /-- If A is an R-algebra all of whose elements are integral over R,
336  and x is an element of an A-algebra that is integral over A, then x is integral over R.-/
337  lemma is_integral_trans (A_int : ∀ x : A, is_integral R x) (x : B) (hx : is_integral A x) :
id                                            └─────────┘                 └─────────┘  
src                                            └─────────┘                    └─────────┘
typ                                           └─────────┘                 └─────────┘  
338    is_integral R (comap.to_comap R A B x) :=
id     └─────────┘   └────────────┘    
src    └─────────┘    └────────────┘
typ    └─────────┘   └────────────┘    
339  begin
st   └─────
340    rcases hx with ⟨p, pmonic, hp⟩,
id            └┘
src    └─────┘  └───────────────────┘
typ    └─────┘└┘└───────────────────┘
doc    └─────┘  └───────────────────┘
txt    └─────┘  └───────────────────┘
par    └─────┘  └───────────────────┘
pid            └───────────────────┘
st   ───────────────────────────────┘
341    let S : set (comap R A B) :=
id             └─┘  └───┘   
src        └─┘  └───┘     
typ        └─┘  └───┘  
doc             └───┘     
txt                       
par                       
pid                       
st   └─┘    └─┘ └───────────┘  
342      (↑((finset.range (p.nat_degree + 1)).image
id          └──────────┘  └──────────┘ 
src       └──────────┘  └──────────┘      
typ       └──────────┘  └──────────┘      
doc        └──────────┘  └──────────┘       
txt                                         
par                                         
pid                                         
st     └───────────┘   └───────────┘      
343        (λ i, to_comap R A B (p.coeff i))) : set (comap R A B)),
id               └──────┘     └─────┘        └─┘  └───┘
src         └──────┘    └─────┘     └─┘ └───┘       
typ         └──────┘ └─────┘     └─┘ └───┘       
doc                     └─────┘         └───┘       
txt                                                 
par                                                 
pid                                                 
st      └─┘  └─┘ └─┘ └─┘ └─┘ └─┘ └─┘    └─┘  └─┘     
344    refine is_integral_of_mem_of_fg (adjoin R (S ∪ {comap.to_comap R A B x})) _ _ _,
id                                                                       
typ                                                                      
345    swap, { apply subset_adjoin, simp },
st                                       └┘
346    apply fg_trans,
347    { apply fg_adjoin_of_finite, { apply finset.finite_to_set },
st                                                               └┘
348      intros x hx,
349      rw [finset.mem_coe, finset.mem_image] at hx,
350      rcases hx with ⟨i, hi, rfl⟩,
351      rcases A_int (p.coeff i) with ⟨q, hq, hqx⟩,
id                             
typ                            
352      use [q, hq],
353      replace hqx := congr_arg (to_comap R A B : A → (comap R A B)) hqx,
id                                            
typ                                           
354      rw alg_hom.map_zero at hqx,
355      convert hqx using 1,
356      symmetry, exact polynomial.hom_eval₂ _ _ _ _ },
st                                                    └┘
357    { apply fg_adjoin_singleton_of_integral,
358      exact is_integral_trans_aux _ pmonic hp _ rfl }
st                                                     └─
359  end
st   ──┘
360  
361  /-- If A is an R-algebra all of whose elements are integral over R,
362  and B is an A-algebra all of whose elements are integral over A,
363  then all elements of B are integral over R.-/
364  lemma algebra.is_integral_trans (A_int : ∀ x : A, is_integral R x)(B_int : ∀ x:B, is_integral A x) :
id                                                                                              
typ                                                                                             
365    ∀ x:(comap R A B), is_integral R x :=
id                                 
typ                                
366  λ x, is_integral_trans A_int x (B_int x)
id                                       
typ                                      
367  
368  end algebra